Inference at * 1 
Iof proof for Lemma can-apply-compose-iff:



1. A : Type
2. B : Type
3. C : Type
4. g : A(B + Top)
5. f : B(C + Top)
6. x : A
7. can-apply(g;x)
8. can-apply(f;do-apply(g;x))
  can-apply(f o g  ;x) 

latex

 by ((All (RepUR ``can-apply p-compose``)) 
CollapseTHEN ((((if (0
Co) =0 then SplitOnConclITE else SplitOnHypITE (0))) 
THEN (Auto)))) 

latex

TH.

Definitions	f o g  , can-apply(f;x), left + right, Unit, t  T, P  Q, P & Q, x:A  B(x), b, s = t, , x:A. B(x), x:AB(x), A, P  Q, False
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot